P:, d:Dec(P). ([d])  (([d])) 

latex

ProofTree

Definitions	P  Q, P & Q, x:A  B(x), x. t(x), P  Q, P  Q, b, [d], , x.A(x), x:A. B(x), P  Q, left + right, A, x:AB(x), Dec(P), , Type, t  T
Lemmas	not wf, assert wf, dcdr-to-bool wf, decidable wf, dcdr-to-bool-equivalence, not functionality wrt iff, or functionality wrt iff, all functionality wrt iff